\chapter{Experimentos y resultados}
\label{Chapter4}
\lhead{Capítulo 4. \emph{Experimentos y resultados}}

Este capítulo presenta una serie de experimentos realizados para evaluar hasta
qué punto es práctico resolver problemas en NP y PH modelados en lógica y
traducidos por la herramienta.
En primer lugar, se justifica la escogencia de un planificador basado en SAT
para la realización de los experimentos y se presenta una forma de calcular
cotas inferiores y superiores para acotar la búsqueda de una solución. Luego,
se explica el protocolo de realización de los experimentos y se describen brevemente 
los problemas en NP y PH que se utilizarán. Finalmente, se discuten los resultados
obtenidos en estos experimentos.

\section{Escogencia del planificador}
De acuerdo con \cite{russell:book}, las estrategias más comunes para resolver
un problema de planificación son la utilización de planificadores basados en
SAT (SAT-\textit{planners}), la búsqueda heurística y la búsqueda basada en un
grafo de planificación.

\cite{rintanen:notes} expone que para ciertos dominios es conveniente
considerar la noción de planes paralelos: planes que permiten la aplicación de
varias acciones ``a la vez'': si existen $n$ acciones que afectan y dependen de
condiciones disjuntas, hay $n!$ planes que son equivalentes (i.e., llevan al
mismo estado) que serían explorados por un planificador serial. Si $n$ es
grande, esto puede ser combinatoriamente complejo. Por tanto, un planificador
que tome en cuenta planes paralelos tendría ventajas sobre un planificador
serial.

Recuerde que en los dominios traducidos por la herramienta propuesta en este
trabajo, las acciones \texttt{colocar-verdadera}
aplicadas a diferentes variables o tuplas son completamente independientes, y
por tanto paralelizables.

Existen planificadores basados en SAT que resuelven problemas de
planificación paralela de manera muy eficiente. Se escogió el
SAT-\textit{planner} del
estado del arte \texttt{M} \citep{rintanen:m2010} para realizar los experimentos, 
debido a su superior desempeño.

\subsection{Ventanas de horizonte para la traducción de NP}

En esta sección se derivan cotas estrictas sobre la longitud de los planes
paralelos para los problemas resultantes. Estas cotas se utilizan con un
planificador basado en SAT para demostrar que un problema STRIPS no tiene
solución o para mejorar el desempeño de los planificadores.

Una ventana de horizonte para un problema STRIPS $P$ es un intervalo de la
forma $[i,f]$, tal que $P$ tiene solución si y sólo si tiene un plan paralelo 
de tamaño $\ell\in[i,f]$. Las ventanas se pueden utilizar para podar el espacio de
búsqueda.

La estructura recursiva del problema generado permite el cálculo de ventanas de
horizonte no triviales. Como todas las acciones \texttt{colocar-verdadera}
pueden ser aplicadas de manera concurrente, un plan paralelo necesita a lo sumo un paso para
ejecutarlas. El plan también requiere de las acciones \texttt{empezar-prueba}
y \texttt{probar-meta}. De este modo, la ventana de horizonte es $[2,3]$ más la
ventana de horizonte $\pwin(\psi)$ de la sentencia $\psi$. Las ventanas de
horizonte son definidas inductivamente por

\begin{enumerate}[--]
\item $\pwin(\theta)\doteq [0,0]$ si $\theta$ es un literal,
\item $\pwin(\wedge_{i=1}^n \theta_i)\doteq 1+\bigvee_{i=1}^n \pwin(\theta_i)$,
\item $\pwin(\vee_{i=1}^n \theta_i)\doteq 1+\bigwedge_{i=1}^n \pwin(\theta_i)$,
\item $\pwin((\exists y)\theta(\bar x,y))\doteq 1+\pwin(\theta)$, y
\item $\pwin((\forall y)\theta(\bar x,y))\doteq \|A\|+\pwin(\theta)$,
\end{enumerate}
donde $\A$ es la estructura asociada al problema, y las operaciones entre
ventanas y escalares son
$[a,b]\vee[a',b']\doteq[\max(a,a'),\max(b,b')]$,
$[a,b]\wedge[a',b']\doteq[\min(a,a'),\max(b,b')]$ y
$c+[a,b]\doteq[c+a,c+b]$.

SAT, por ejemplo, tiene la ventana $[\|\A\|+5,\|\A\|+6]$,
lo que significa que el CNF codificado por la estructura $\A$ es satisfacible
si y sólo si existe un plan paralelo de longitud $\|\A\|+5\leq\ell\leq\|\A\|+6$.

\subsection{Ventanas de horizonte para la traducción de PH}
%Given a SO formula $\Phi$ describing property $\Pi$ and a
%structure $\A$ encoding an instance of the problem, one
%wants to decide whether the instance satisfy the property
%or not; i.e., $\A\models\Phi$. The tool just described 
%generates in polytiempo (in the size $\|\A\|$) an \STRIPS
%problem $P$ that has solution iff $\A\models\Phi$.
%Thus, $P$ can be solved with any complete planner to
%answer the original question. However, SAT-based planners
%are inherently incomplete when there is no solution as
%they continue the search forever unless an upper bound
%on the length of the plan is given in advance.\footnote{Of
%course, $2^n$ where $n$ is the number of fluents in $P$
%is a trivial upper bound. Clearly, for $n\geq100$ (or less)
%such a bound is inconsequential. Very often problems have
%more than 100 fluents.}

En esta sección se muestra cómo calcular cotas superiores e inferiores estrictas
sobre la longitud de planes paralelos para fórmulas $\Phi \in$ \LSO.
Como en la sección anterior, se procede inductivamente sobre la estructura de $\Phi$:
\begin{enumerate}[1.]
\item si $\Phi=\psi$ (fórmula de primer orden), entonces $\pwin(\Phi)=\pwin(\psi)$.
\item si $\Phi=(\exists R^t)\Psi$, entonces $\pwin(\Phi)=3+[\![\pwin=u]\!]+\pwin(\Psi)$.
\item si $\Phi=(\forall R^t)\Psi$, entonces
  $\pwin(\Phi)=2^{\#t} \cdot \pwin(\Psi)+3 - 1 $%   2^{\#t+1}+2^{\#t}\pwin(\Psi)=2^{\#t}[2+\pwin(\Psi)]$
\ , donde\\
  $\#t$ es el número de tuplas de tipo $t$,\\ 
  $2^{\#t}$ es el número de relaciones $R$, \\
  y $2^{\#t+1}-2$ es el número de bits cambiados cuando se incrementa un
contador de $\#t$ bits desde cero hasta su máximo \citep{cormen:algorithms}.
\end{enumerate}
En 2, $[\![\pwin=u]\!]$ es 1 o 0 dependiendo de si $\pwin$ se refiere a la cota
superior $u$ o no.

%upper bound $u$ or not. It is not hard to see that one
%can get the unique expression $\pwin(\Phi)=4+\pwin(\Psi)$ for the
%lower and upper bounds in 2 by pushing the lower bound 1 unit.
%By bounding the upper limit of parallel horizon 
%windows, we obtain the following surprising result.
%
%\begin{theorem}
%Consider a signature $\sigma$, $\Phi\in\SOE(\sigma)$ and
%$\A\in\struc[\sigma]$. Then, to decide $\A\models\Phi$,
%it is enough to consider parallel plans of makespan
%linear on $\|\A\|$ for fixed $\Phi$ but independently
%of the arities in $\sigma$ and $\Phi$.
%More precisely, it is enough to consider plans of makespan
%at most $q(\|\A\|-1)+d+3$ where $q$ is the maximum nesting
%of universal quantifiers in $\psi$, $d$ is the depth of
%$\psi$ and $\psi$ is the FOL part of $\Phi$.
%\end{theorem}
%\begin{proof}
%Let $n=\|\A\|$ and $T$ the parse tree of height $h$ for $\psi$.
%For a maximal branch $b\in T$, let $q_b$ be the number
%of universal quantifiers in $b$, $h_b$ its height, and
%$u(b)$ the upper limit of the parallel horizon window
%along $b$. The upper limit $u(\psi)$ of $\pwin(\psi)$
%is $\max_{b\in T} u(b)$. On the other hand,
%\[ u(b) = q_bn + h_b - q_b = q_b(n-1) + h_b \leq q(n-1) + h. \]
%End with $h=d$ and that $3$ must be added to $u(\psi)$.
%\end{proof}
%
%This bound is tight for SAT.
%The result is surprising because one would expect 
%the need to consider parallel plans of makespan $\O(\|\A\|^k)$
%for some $k$. However, note that a linear makespan
%does not mean a linear number of operators.

\section{Diseño de los experimentos}
%En esta sección se describe el protocolo experimental utilizado
%en este trabajo.

\subsection{Procedimiento}

Los experimentos consistieron en la modelación, traducción y resolución
de problemas NP y PH. Para cada tipo de problema se ejecutó el planificador
\texttt{M} sobre instancias de
distintos tamaños y características, para luego analizar cuántos y cuáles
instancias fueron resueltas satisfactoriamente en un tiempo limitado, y cuáles
fueron los tiempos de corrida.
Los detalles sobre la modelación de cada problema pueden encontrarse en el
Apéndice \ref{apendiceA}.

Es importante recalcar que, como se ha demostrado la correctitud de la
herramienta, \textbf{siempre se puede hallar una solución (si la instancia es
positiva) o demostrar que no existe tal solución (si la instancia es
negativa)}. Como no se dispone de máquinas con cantidad arbitraria de memoria
ni de tiempo ilimitado, en las tablas de resultados se refleja la cantidad de
problemas a los que el computador pudo responder dentro de sus límites. Esto no
quiere decir que la herramienta falla en algunos casos, sino que la complejidad
de un problema puede exceder la cantidad de tiempo y espacio prefijado para su
resolución.

\section{Experimentos y resultados de problemas NP}
Se realizaron experimentos en los problemas NP-completos: \SAT, \CLIQUE, \CHD
\ (Camino \textit{Hamiltoniano} Dirigido),
\TDM\ (\textit{3-Dimensional Matching}), \TCOL\ (3-colorabilidad) y \KCOL
\ ($k$-colorabilidad).
También se computó el número cromático de grafos aleatorios utilizando la
herramienta como un oráculo.

Los experimentos se realizaron en un procesador Intel Xeon corriendo a 1.86 GHz,
con 2 GB de memoria RAM. Cada instancia se intentó resolver utilizando el
planificador \texttt{M} durante 30 minutos, con un límite de 1GB de memoria.

A continuación se presentan los resultados desglosados por dominio.
Para cada tipo de problema, la tabla muestra el número de instancias resueltas
($N^*$), el número total de instancias ($N$), el número de instancias resueltas
que satisfacen la propiedad (\#pos), el número de instancias resueltas que
\textbf{no} satisfacen la propiedad (\#neg), y el tiempo promedio de resolución
en segundos. Sobre cada tabla se incluye el tamaño de la ventana de horizonte
particular del problema ($\pwin$).

\subsection{SAT}
Las instancias de SAT fueron tomadas del repositorio
SATLIB\footnote{\texttt{http://www.satlib.org}}, un sitio web hecho por
\cite{hoos:satlib} que aloja una librería de problemas SAT que pertenecen a la
región de la \textit{fase de transición} \citep{gent:transition}, es decir,
tienen ciertas propiedades que los hacen difíciles de resolver.
Los problemas de tipo uf20, uf50 y uf75 son instancias aleatorias con 20, 50 y
75 variables proposicionales, respectivamente, mientras que las instancias de
tipo uuf50 y uuf75 son no satisfacibles de tamaño 50 y 75.

\begin{table}[h!]
\begin{center}
\begin{tabular}{lllllll}
\multicolumn{5}{@{}c}{\footnotesize\SAT: $\pwin=[n+5,n+6]$} \\
\midrule
              &    $N^*$/$N$ & \#pos. & \#neg. & tiempo prom. (seg) \\
\midrule
%                                                             % sample standard deviation
uf20          &        40/40 &     40 &      0 &       1.7 \\ % 2.0
uf50          &        40/40 &     40 &      0 &     146.7 \\ % 202.3
uf75          &        15/40 &     15 &      0 &     362.1 \\ % 568.6
uuf50         &        40/40 &      0 &     40 &     548.5 \\ % 260.2
uuf75         &         1/40 &      0 &      1 &   1,746.4 \\ % 0.0
\midrule
\end{tabular}
\end{center}
\caption[Resultados de M para \SAT]{Resultados de M para \SAT}
%\label{table:results}
\end{table}

M fue capaz de resolver todos los problemas pequeños de SAT, tardándose más en
las instancias no satisfacibles (para probar que no había solución). El límite
de lo resoluble por el planificador con las restricciones fijadas estuvo entre las 50 y 75 variables.

\subsection{Problemas de grafos y \TDM}
Las instancias de problemas de grafos se generaron de acuerdo con el modelo
$G(n, p)$ de \cite{bollobas:random-graphs}; es decir, grafos de $n$ nodos con $p$ probabilidad de ocurrencia de
cada arista. Las instancias para \TDM\ se generaron
escogiendo aleatoriamente tripletas de $\{0,\ldots,n-1\}^3$ con probabilidad
$p$, siendo $p$ variable. 

\begin{table}[h!]
\begin{center}
\begin{tabular}{lllllll}
\multicolumn{5}{@{}c}{\footnotesize\textsc{Clique}: $\pwin=[2n+4, 3n+7]$} \\
\midrule
              &    $N^*$/$N$ & \#pos. & \#neg. & tiempo prom. (seg) \\
\midrule
%5-3           &        40/40 &     10 &     30 &       0.0 \\ % 0.0
%5-4           &        40/40 &      0 &     40 &       0.2 \\ % 0.5
10-3          &        40/40 &     22 &     18 &       1.2 \\ % 0.8
10-4          &        40/40 &     12 &     28 &       2.2 \\ % 2.3
10-5          &        40/40 &      1 &     39 &      32.3 \\ % 106.7
15-3          &        40/40 &     22 &     18 &      10.5 \\ % 8.2
15-4          &        40/40 &     11 &     29 &      36.6 \\ % 84.5
15-5          &        39/40 &      4 &     35 &      74.3 \\ % 136.2
15-6          &        37/40 &      1 &     36 &      79.4 \\ % 128.3
20-3          &        40/40 &     25 &     15 &      40.2 \\ % 21.6
20-4          &        40/40 &     17 &     23 &      72.6 \\ % 66.3
20-5          &        39/40 &     10 &     29 &     159.6 \\ % 252.4
20-6          &        34/40 &      4 &     30 &     185.2 \\ % 225.2
25-3          &        40/40 &     30 &     10 &     111.9 \\ % 53.9
25-4          &        40/40 &     18 &     22 &     231.0 \\ % 236.7
25-5          &        39/40 &     10 &     29 &     387.5 \\ % 396.6
25-6          &        36/40 &      8 &     28 &     394.1 \\ % 321.1
\end{tabular}
\end{center}
\caption[Resultados de M para \CLIQUE]{Resultados de M para \CLIQUE. Se utiliza
la notación $x-y$ para denotar que el problema fue hallar una clique de tamaño
$y$ en un grafo con $x$ nodos.}
%\label{table:results}
\end{table}

Es interesante que la herramienta sea capaz de producir problemas de
\textit{clique} resolubles en menos de cinco minutos para grafos de hasta 25 nodos, sin la
utilización de ninguna heurística ni optimización específica al problema.

\begin{table}[h!]
\begin{center}
\begin{tabular}{lllllll}
\multicolumn{5}{@{}c}{\footnotesize\CHD: $\pwin=[n+3,n+10]$} \\
\midrule
              &    $N^*$/$N$ & \#pos. & \#neg. & tiempo prom. (seg) \\
\midrule
%5             &        40/40 &     12 &     28 &       0.0 \\ % 0.0
10            &        40/40 &     15 &     25 &       1.1 \\ % 2.3
15            &        39/40 &     18 &     21 &      63.7 \\ % 203.3
20            &        31/40 &     20 &     11 &      70.0 \\ % 127.6
25            &        29/40 &     20 &      9 &     202.1 \\ % 199.8
30            &        22/40 &     20 &      2 &     629.1 \\ % 242.2
\midrule
\end{tabular}
\end{center}
\caption[Resultados de M para \CHD]{Resultados de M para \CHD. La primera
columna indica el número de nodos del grafo.}
%\label{table:results}
\end{table}

El planificador tuvo mayores dificultades en este dominio que en el anterior, a
juzgar por la cantidad de problemas resueltos con el mismo número de nodos.

\begin{table}[h!]
\begin{center}
\begin{tabular}{lllllll}
\multicolumn{5}{@{}c}{\footnotesize\TDM: $\pwin=[3n+4,3n+6]$} \\
\midrule
              &    $N^*$/$N$ & \#pos. & \#neg. & tiempo prom. (seg) \\
\midrule
%5             &        40/40 &     19 &     21 &       0.0 \\ % 0.0
10            &        40/40 &     36 &      4 &       9.6 \\ % 2.8
15            &        40/40 &     40 &      0 &     251.5 \\ % 65.5
20            &        13/40 &     13 &      0 &   1,191.0 \\ % 42.1 (avg/std) is over 3 instances !!!
25            &         0/40 &      0 &      0 &       -- \\ % --
\midrule
\end{tabular}
\end{center}
\caption[Resultados de M para \TDM]{Resultados de M para \TDM. La primera
columna indica la cardinalidad del conjunto.}
%\label{table:results}
\end{table}

\TDM\ es un dominio particularmente difícil: como la cota inferior es $3n+4$, 
el planificador debe empezar a buscar planes que son más largos que en los
dominios anteriores. De cualquier modo, es conveniente poder resolver este problema 
de hipergrafos para instancias pequeñas utilizando sólo planificación automática
en lugar de un \textit{software especializado}, gracias a la herramienta.

\begin{table}[h!]
\begin{center}
\begin{tabular}{lllllll}
\multicolumn{5}{@{}c}{\footnotesize\TCOL: $\pwin=[2n+4, 2n+7]$} \\
\midrule
              &    $N^*$/$N$ & \#pos. & \#neg. & tiempo prom. (seg) \\
\midrule
%5             &        40/40 &     37 &      3 &       0.0 \\ % 0.0
10            &        40/40 &     18 &     22 &       0.1 \\ % 0.1
15            &        40/40 &     24 &     16 &       0.9 \\ % 0.6
20            &        40/40 &     12 &     28 &       3.0 \\ % 1.8
25            &        40/40 &     30 &     10 &       8.9 \\ % 4.7
30            &        40/40 &      9 &     31 &      20.9 \\ % 12.2
40            &        40/40 &      4 &     36 &      75.1 \\ % 55.7
50            &        40/40 &      1 &     39 &     196.7 \\ % 119.2
\midrule
\end{tabular}
\end{center}
\caption[Resultados de M para \TCOL]{Resultados de M para \TCOL. La primera
columna indica el número de nodos del grafo.}
%\label{table:results}
\end{table}

\TCOL\ fue el dominio que arrojó las mejores resultados, comparándolo con otros
problemas de grafos de tamaño similar. Nótese que en la mayoría de los casos de
los grafos más grandes no existía una 3-coloración válida, y la ventana de
horizontes le permitió al planificador dar una respuesta en un tiempo
relativamente corto.

\begin{table}[h!]
\begin{center}
\begin{tabular}{lllllll}
\multicolumn{5}{@{}c}{\footnotesize\KCOL: $\pwin=[2n+4,3n+6]$} \\
\midrule
              &    $N^*$/$N$ & \#pos. & \#neg. & tiempo prom. (seg) \\
\midrule
%5-2           &        40/40 &     20 &     20 &       0.0 \\ % 0.0
%5-3           &        40/40 &     37 &      3 &       0.0 \\ % 0.0
%5-4           &        40/40 &     39 &      1 &       0.0 \\ % 0.0
10-2          &        40/40 &      9 &     31 &       1.9 \\ % 0.5
10-3          &        40/40 &     18 &     22 &       2.8 \\ % 1.4
10-4          &        40/40 &     27 &     13 &      11.0 \\ % 23.3
15-2          &        40/40 &      7 &     33 &      33.5 \\ % 9.2
15-3          &        40/40 &     16 &     24 &      46.5 \\ % 12.3
15-4          &        40/40 &     24 &     16 &      91.7 \\ % 113.5
20-2          &        40/40 &      3 &     37 &     254.9 \\ % 68.2
20-3          &        40/40 &     12 &     28 &     395.9 \\ % 221.8
20-4          &        40/40 &     20 &     20 &     497.3 \\ % 178.0
25-2          &         0/40 &      0 &      0 &       -- \\ % --
25-3          &         0/40 &      0 &      0 &       -- \\ % --
25-4          &         0/40 &      0 &      0 &       -- \\ % --
\midrule
\end{tabular}
\end{center}
\caption[Resultados de M para \KCOL]{Resultados de M para \KCOL. La primera
columna indica el número de nodos del grafo y el número de colores de los que
se intenta colorear.}
%\label{table:results}
\end{table}

Los problemas de \KCOL\ arrojaron buenos resultados hasta considerar los
grafos de 25 nodos, para los cuales no se halló ninguna solución dentro de los
30 minutos por problema que se le dio al computador. Esto muestra que la
dificultad de los problemas NP escala muy rápidamente, incluso cuando hay aumentos
pequeños en el tamaño del problema.

En total, de todos los 1920 problemas que se intentó resolver, fueron
solucionadas 1614 instancias (el 84\%), 706 de las cuales eran positivas (es
decir, se consiguió un plan que solucionaba el problema.

\subsection{Número cromático}

El número cromático $\chi$ de un grafo $G=(V,E)$ es el menor $k$ tal que $G$ es
$k$-coloreable. Determinar este número es un problema NP-hard, pero puede
hacerse probando su $k$-colorabilidad por valores incrementales\footnote{Esto
se puede mejorar realizando una búsqueda binaria en $k$.} de
$k=1,\ldots,|V|$.

La Tabla \ref{chromatic} muestra los detalles de corrida de ocho instancias de
grafos a los cuales se les determinó su número cromático utilizando la
herramienta y el planificador M como un oráculo para decidir
la colorabilidad para distintos $k$.

\begin{table}[h!]
\centering
\small
\begin{tabular}{lllllllll}
       &       & \multicolumn{7}{c}{$k$-colorabilidad} \\
\cmidrule(l){3-9}
instancia      & $\chi$ &     1 &     2 &     3 &     4 &     5 &     6 &     7 \\
\midrule
10-0.75 (1)      &      5 &     2 &     2 &     6 &   101 &\bf  3 &       &       \\
10-0.75 (2)      &      5 &     1 &     2 &     2 &     6 &\bf  4 &       &       \\
10-0.85        &      7 &     2 &     2 &     3 &     6 &     4 & 1,265 &\bf  4 \\
15-0.25        &      2 &    27 &\bf 62 &       &       &       &       &       \\
15-0.60        &      5 &    27 &    29 &    54 &   118 &\bf 72 &       &       \\
15-0.70        &      6 &    28 &    28 &    33 &    47 &   329 &\bf 67 &       \\
20-0.10        &      3 &   214 &   350 &\bf705 &       &       &       &       \\ % last number strange
20-0.25        &      4 &   211 &   272 & 1,261 &\bf837 &       &       &       \\
\midrule
\end{tabular}
\caption[Resultados de M sobre números cromáticos]{
Resultados de M sobre el cómputo de números cromáticos en grafos aleatorios.
La primera columna muestra el número de nodos del grafo y su probabilidad según
el modelo $G(n,p)$.
Para cada instancia, la tabla muestra el número cromático $\chi$, el tiempo
(en segundos) para demostrar o descartar la $k$-colorabilidad para valores
incrementales de $k$.
El último valor de $k$ para cada instancia es el número cromático.}
\label{chromatic}
\end{table}

Nótese que los mayores tiempos de corrida corresponden normalmente a
la prueba de $k$-colorabilidad para $k = \chi - 1$. Esto se debe a que
para un grafo con número cromático $\chi$
no es trivial descartar que sea $(\chi - 1)$-coloreable, y el programa debe
agotar todas las posibles formas de colorearlo antes de rendirse e intentar con
un color adicional. No se logró determinar qué propiedad del grafo causó
mayores tiempos de corrida en el último valor de $k$ para las instancias 15-0.25 y 20-0.10.

\section{Experimentos y resultados de problemas PH}
Se llevaron a cabo diferentes experimentos para probar la dificultad de los
problemas generados. Las dos categorías de problemas estudiados fueron QBF, un
problema que se ubica en PH, y el complemento al problema de 3-colorabilidad de
un grafo, \coCOL, perteneciente a la clase co-NP.
Para QBF se utilizó M, el mismo planificador basado en SAT con el que se
resolvieron los problemas NP. Para \coCOL se utilizó otro planificador del
estado del arte, llamado LAMA'11 \citep{richter:lama}.

Los experimentos se ejecutaron en un CPU Xeon 5140 corriendo a 2.33 GHz,
con 2 GB de RAM y un tiempo límite de una hora y media.

\subsection{QBF}
Se realizaron experimentos sobre varios tipos de problemas QBF
(\textit{quantified Boolean formula}). QBF es una generalización de SAT
en la cual se tiene una fórmula CNF con variables cuantificadas existencial o
universalmente. Por ejemplo, la fórmula
\[ (\exists y_1y_2)\ (\forall x_1x_2) \ ((x_1 \lor \neg y) \land (\neg x_2 \lor
    y) \land (\neg x_1 \lor \neg y_2 \lor y_1)) \]
expresa el problema de hallar una asignación de verdad para $y_1$ y $y_2$ tal
que la fórmula interna sea satisfecha por todas las posibles asignaciones de
verdad de $x_1$ y $x_2$.
Los QBF estudiados, que se ubican en los niveles iniciales de la jerarquía
polinomial, son de la forma siguiente:

\begin{center}
\begin{tabular}{c|c}
Forma del QBF & clase de complejidad\\
\hline
\qEA & $\Sigma_p^2$\\
\qAE & co-$\Sigma_p^2$\\ 
\qEAE & $\Sigma_p^3$\\
\qAEA & co-$\Sigma_p^3$\\
\end{tabular}
\end{center}

Por ejemplo, la fórmula $\Phi$ para \qAE-QBF es:
\begin{alignat*}{1}
\label{eq:qbf:ea}
&(\forall T_1^{\text{V}_1})(\exists T_2^{\text{V}_2})(\forall y\in\text{Cls})(\exists x\in\text{Var}) \\
&\quad \bigl[P(x,y) \land [(\text{V}_1(x) \land T_1(x))\lor(\text{V}_2(x) \land T_2(x))]\bigr]\ \lor \\
&\quad \bigl[N(x,y) \land [(\text{V}_1(x) \land \neg T_1(x))\lor(\text{V}_2(x) \land \neg T_2(x))]\bigr]
\end{alignat*}
donde $V_1$ y $V_2$ son tipos que particionan las variables en universales y
existenciales.

Se presentan los resultados de resolver, utilizando el planificador M, 
los cuatro tipos de problemas QBF mencionados,
traducidos por la herramienta. Las instancias son aleatorias,
generadas con \textsc{BlocksQBF}\footnote{\url{http://fmv.jku.at/blocksqbf}},
%!incluir referencia
que está basado en el modelo aleatorio de \cite{chen:random:qbf}. Cada
problema tiene 150 cláusulas. En las columnas de las tablas se muestra
el número de variables de cada tipo, el número de
instancias que se intentaron resolver ($n$), el número de instancias
resueltas con solución ($+$) y en las que no hay solución ($-$), y promedios
de tiempo en segundos y longitud del plan paralelo (para las instancias
resueltas donde hay solución).

\begin{table}[h!]
\centering
  \begin{tabular}{lllrrrrrrrrrl}
    \multicolumn{10}{@{}c}{\footnotesize\qEA-QBF} \\
    \midrule
    %\toprule
    & $\#\exists$ & $\#\forall$ &             & $n$ & $+$ & $-$ & tiempo (seg) &   long. plan &  \\
    \midrule
          &          60 &           1 &             &   5 & -- &   5 &   184.3 &    -- &  \\
          &             &           2 &             &   5 & -- &   1 & 4,382.5 &    -- &  \\
    \cmidrule{2-10}
          &         100 &           1 &             &   5 &   4 &   1 &   176.6 &   316 &  \\ % #actions=36,017
          &             &           2 &             &   5 &   3 &   2 & 3,471.9 &   628 &  \\ % #actions= 2,737
    \midrule
  \end{tabular}
\end{table}

De los problemas QBF-\qEA con 60 variables existenciales y una universal fueron
resueltos en tiempos relativamente cortos, aunque no al nivel de un
solucionador especializado de problemas QBF.
Es probable que las instancias con 60 variables existenciales
y 2 universales no tuvieran ninguna solución, pero el planificador no pudo
determinarlo porque fue abortado al agotarse el tiempo estipulado para los
experimentos. Con 100 variables existenciales, el planificador encuentra
soluciones con mayor facilidad. El incremento de tiempo al agregar una sola
variable universal adicional es enorme, pues debe construirse una prueba para
todos los modelos posibles de dos variables independientes.

\begin{table}[h!]
\centering
  \begin{tabular}{lllrrrrrrrrrl}
    \multicolumn{10}{@{}c}{\footnotesize\qEAE-QBF} \\
    \midrule
    & $\#\exists$ & $\#\forall$ & $\#\exists$ & $n$ & $+$ & $-$ & tiempo (seg) &   long. plan &  \\
    \midrule
          &          10 &           2 &          30 &   5 & -- &   5 & 4,199.2 &    -- &  \\
          &             &           2 &          50 &   5 & -- &   5 & 2,313.9 &    -- &  \\
    \cmidrule{2-10}
          &          30 &           2 &          30 &   5 & -- &   5 & 3,210.7 &    -- &  \\
          &             &           2 &          50 &   5 & -- &   5 & 3,166.3 &    -- &  \\
    \cmidrule{2-10}
          &          50 &           2 &          30 &   5 & -- &   1 & 3,313.4 &    -- &  \\
          &             &           2 &          50 &   5 &   3 &   2 & 3,450.9 &   640 &  \\ % #actions=3,182.0
    \midrule
  \end{tabular}
\end{table}
%! por qué no experimentos con una sola variable universal?

El planificador pudo determinar que la mayoría de los problemas \qEAE-QBF no
tenían solución. Los tiempos fueron cercanos al límite de 1.5 horas, y los
planes no fueron significativamente más largos que en los problemas \qEA-QBF,
debido a que se mantuvo fijo el número de variables universales (que son las
responsables por un crecimiento exponencial en el tamaño del plan).

\begin{table}[h!]
\centering
  \begin{tabular}{lllrrrrrrrrrl}
    \multicolumn{10}{@{}c}{\footnotesize\qAE-QBF} \\
    \midrule
    & $\#\forall$ & $\#\exists$ &             & $n$ & $+$ & $-$ & tiempo (seg) & long. plan &  \\
    \midrule
          &           1 &         100 &             &   5 &   5 & -- &   147.9 &   319 &  \\ % #actions=45,378.6
    \cmidrule{2-10}
          &           2 &          30 &             &   5 & -- &   5 & 2,060.4 &    -- &  \\
          &             &          60 &             &   5 &   4 &   1 & 3,100.7 &   637 &  \\ % #actions=3,086.0
          &             &          80 &             &   5 &   5 & -- & 2,893.2 &   637 &  \\ % #actions=2,961.4
          &             &         100 &             &   5 &   5 & -- & 2,092.8 &   637 &  \\ % #actions=3,171.8
    \cmidrule{2-10}
          &           3 &          15 &             &   5 & -- & -- &      -- &    -- &  \\
    \midrule
    %\bottomrule
  \end{tabular}
\end{table}

Los tiempos y longitudes en los problemas \qAE-QBF fueron muy similares a los
de problemas complementarios \qEA-QBF. Como era de esperarse, las instancias
con más de dos variables universales no pudieron ser resueltos, ni siquiera al
disminuir significativamente el número de variables existenciales buscando que
el planificador pudiera demostrar que los problemas no tienen solución. Para
solucionar estas instancias haría falta mucho más tiempo, y se prevé que la longitud de los
planes sea mucho mayor.

\begin{table}[h!]
\centering
  \begin{tabular}{lllrrrrrrrrrl}
    \multicolumn{10}{@{}c}{\footnotesize\qAEA-QBF} \\
    \midrule
    & $\#\forall$ & $\#\exists$ & $\#\forall$ & $n$ & $+$ & $-$ & tiempo (seg) &   long. plan &  \\
    \midrule
          &           1 &          60 &           1 &   5 &   1 & -- &   404.7 &   635 &  \\
          &             &          60 &           2 &   5 & -- & -- &     -- &    -- &  \\
          &             &          80 &           1 &   5 &   5 & -- &   403.2 &   635 &  \\
          &             &         100 &           1 &   5 &   5 & -- &   390.8 &   635 &  \\
    \cmidrule{2-10}
          &           2 &          60 &           1 &   5 &   2 & -- &   456.7 & 1,269 &  \\
          &             &          60 &           2 &   5 & -- & -- &     -- &    -- &  \\
          &             &          80 &           1 &   5 &   5 & -- &   499.5 & 1,269 &  \\
          &             &         100 &           1 &   5 &   5 & -- &   454.9 & 1,269 &  \\
    %\bottomrule
  \end{tabular}
\end{table}

% por qué los resultados con dos variables externas dan mejor?
Puede resultar curioso que las pruebas de \qAEA-QBF para dos variables
cuantificadas universalmente en el nivel más externo dieron como resultado
mejores tiempos que las del tipo \qEA-QBF que tenían dos variables dependientes
de la cuantificación universal.
Esto se debe a que en estas últimas pruebas había instancias negativas, por lo
que era necesario evaluar todos los posibles valores de la cuantificación
existencial, incurriendo en un mayores tiempos de corrida.

\subsection{\coCOL}
El complemento de \TCOL, \coCOL, es el problema de decisión que pregunta si un
grafo \textbf{no} es 3-coloreable. En el caso de que la respuesta para un grafo
sea afirmativa, la prueba de ello debe mostrar que se realizó la asignación de
los tres colores posibles a todos los nodos del grafo, y en todos los casos
fue imposible probar que la coloración era válida. Este problema está en co-NP,
su formulación detallada se encuentra en el Apéndice \ref{apendiceA}.

Para probar este dominio, se generaron nuevamente grafos aleatorios con el modelo
$G(n,p)$. Los experimentos se realizaron en la misma máquina y con las
mismas restricciones que los experimentos de problemas QBF.

En este caso no se obtuvo buenos resultados con el planificador M.
Los resultados de LAMA'11 \citep{richter:lama} se muestran en la
Tabla \ref{table:exp:co-3col}.

\begin{table}[h!]
\centering
\begin{tabular}{crrrrr}
$|V|$ & $n$ & $+$ & $-$ &  tiempo (seg) & long. plan  \\
\midrule
    4 &   5 &   1 &   4 &   0.6 &   1,731  \\
    5 &   5 &   2 &   3 &  41.0 &   6,695  \\
    6 &   5 &   2 &   3 & 280.3 &  26,163  \\
    7 &   5 &   2 &   2 &  38.2 & 102,935  \\
    8 &   5 &   1 &   2 & 211.9 & 406,851  \\
    9 &   5 & -- &   1 &   0.3 &      -- \\
\end{tabular}
\caption[Resultados de LAMA'11 para \coCOL]{\small \coCOL en grafos aleatorios.
  Las columnas muestran el número de vértices ($|V|$), el número de instancias ($n$),
  el número de instancias positivas ($+$) y negativas ($-$), los tiempos
  promedio en segundos y la longitud del plan de las instancias positivas
  resueltas.
}
\label{table:exp:co-3col}
\end{table}

Sorprendentemente, LAMA'11 es capaz de encontrar planes sumamente largos: en
una instancia consiguió uno con más de 400.000 pasos. Se cree que la razón
por la cual este planificador es capaz de lograr semejante hazaña es que, a diferencia de M, 
es de tipo secuencial y la resolución de problemas en co-NP no requiere de
conjeturas (pues no hay cuantificadores existenciales de segundo orden), sino
de la aplicación lineal de acciones. En este caso llama la atención que el
planificador tardó una gran cantidad de tiempo en el grafo de 6 vértices a
pesar de que la longitud del plan no era excesivamente grande. La razón exacta
de esto es desconocida.

\section{La herramienta en la web}

Para la presentación de este trabajo en la Conferencia Internacional de
Planificación Automática (ICAPS '11) se implementó una sencilla aplicación web
utilizando \textit{Python} y tecnología \textit{CGI}.

La aplicación web consta de una sección en donde el usuario puede introducir
una fórmula $\Phi$ en \LSO\ y una firma $\sigma$ para generar un dominio de
planificación en PDDL, utilizando el lenguaje lógico y la
sintaxis de archivos de texto definidos en el Capítulo 2 sobre campos de texto
libres en la ventana del navegador.
El usuario puede escoger si desea utilizar la primera reducción, diseñada para
problemas NP, o la segunda, que le permite traducir problemas de lógica de
segundo orden general.

Al haber generado un dominio, se le da al usuario la posibilidad de descargar
el dominio traducido en PDDL, y se le presenta otro campo de texto para
permitirle especificar una estructura finita $\A \in \struc[\sigma]$.
Al completar este paso, el usuario tiene la posibilidad de descargar tanto el
dominio como el problema PDDL, archivos que puede utilizar con el planificador
de su preferencia para la resolución de problemas.

En el sitio web también se proveen fórmulas predefinidas para los problemas NP
y PH estudiados en este trabajo, a modo de facilitar el uso de la herramienta
con problemas frecuentes a los potenciales usuarios. Se prevé que la
herramienta web esté disponible bajo el subdominio del Grupo de Inteligencia
Artificial de la Universidad Simón Bolívar, en \url{http://www.gia.usb.ve}.
